Velocity‐based formulations for standard and quasi‐incompressible hypoelastic‐plastic solids

We present three velocity‐based updated Lagrangian formulations for standard and quasi‐incompressible hypoelastic‐plastic solids. Three low‐order finite elements are derived and tested for non‐linear solid mechanics problems. The so‐called V‐element is based on a standard velocity approach, while a mixed velocity–pressure formulation is used for the VP and the VPS elements. The two‐field problem is solved via a two‐step Gauss–Seidel partitioned iterative scheme. First, the momentum equations are solved in terms of velocity increments, as for the V‐element. Then, the constitutive relation for the pressure is solved using the updated velocities obtained at the previous step. For the VPS‐element, the formulation is stabilized using the finite calculus method in order to solve problems involving quasi‐incompressible materials. All the solid elements are validated by solving two‐dimensional and three‐dimensional benchmark problems in statics as in dynamics. Copyright © 2016 John Wiley & Sons, Ltd.     

The cost of probabilistic agreement in oblivious robot networks

In this paper, we look at the time complexity of two agreement problems in networks of oblivious mobile robots, namely, at the gathering and scattering problems. Given a set of robots with arbitrary initial locations and no initial agreement on a global coordinate system, gathering requires that all robots reach the exact same but not predetermined location. In contrast, scattering requires that no two robots share the same location. These two abstractions are fundamental coordination problems in cooperative mobile robotics. Oblivious solutions are appealing for self-stabilization since they are self-stabilizing at no extra cost. As neither gathering nor scattering can be solved deterministically under arbitrary schedulers, probabilistic solutions have been proposed recently.The contribution of this paper is twofold. First, we propose a detailed time complexity analysis of a modified probabilistic gathering algorithm. Using Markov chains tools and additional assumptions on the environment, we prove that the convergence time of gathering can be reduced from O(n²) (the best known bound) to O(1) or , depending on the model of multiplicity detection. Second, using the same technique, we prove that scattering can also be achieved in fault-free systems with the same bounds.     

Non-rigid metric reconstruction from perspective cameras

The metric reconstruction of a non-rigid object viewed by a generic camera poses new challenges since current approaches for Structure from Motion assume the rigidity constraint of a shape as an essential condition. In this work, we focus on the estimation of the 3-D Euclidean shape and motion of a non-rigid shape observed by a perspective camera. In such case deformation and perspective effects are difficult to decouple – the parametrization of the 3-D non-rigid body may mistakenly account for the perspective distortion. Our method relies on the fact that it is often a reasonable assumption that some of the points on the object’s surface are deforming throughout the sequence while others remain rigid. Thus, relying on the rigidity constraints of a subset of rigid points, we estimate the perspective to metric upgrade transformation. First, we use an automatic segmentation algorithm to identify the set of rigid points. These are then used to estimate the internal camera calibration parameters and the overall rigid motion. Finally, we formulate the problem of non-rigid shape and motion estimation as a non-linear optimization where the objective function to be minimized is the image reprojection error. The prior information that some of the points in the object are rigid can also be added as a constraint to the non-linear minimization scheme in order to avoid ambiguous configurations. We perform experiments on different synthetic and real data sets which show that even when using a minimal set of rigid points and when varying the intrinsic camera parameters it is possible to obtain reliable metric information.     

Bond graph based control of a three-phase inverter with LC filter – Connection to passive and active loads

This paper proposes a model of a three phase electrical inverter with a LC output filter in delta connection used in a renewable energy supply system. The concept of inverse bond graph via bicausality is used for the control law design. The control law robustness is tested by connecting passive and active (induction machine) loads.     

iLogDemons: A Demons-Based Registration Algorithm for Tracking Incompressible Elastic Biological Tissues

Tracking soft tissues in medical images using non-linear image registration algorithms requires methods that are fast and provide spatial transformations consistent with the biological characteristics of the tissues. LogDemons algorithm is a fast non-linear registration method that computes diffeomorphic transformations parameterised by stationary velocity fields. Although computationally efficient, its use for tissue tracking has been limited because of its ad-hoc Gaussian regularisation, which hampers the implementation of more biologically motivated regularisations. In this work, we improve the logDemons by integrating elasticity and incompressibility for soft-tissue tracking. To that end, a mathematical justification of demons Gaussian regularisation is proposed. Building on this result, we replace the Gaussian smoothing by an efficient elastic-like regulariser based on isotropic differential quadratic forms of vector fields. The registration energy functional is finally minimised under the divergence-free constraint to get incompressible deformations. As the elastic regulariser and the constraint are linear, the method remains computationally tractable and easy to implement. Tests on synthetic incompressible deformations showed that our approach outperforms the original logDemons in terms of elastic incompressible deformation recovery without reducing the image matching accuracy. As an application, we applied the proposed algorithm to estimate 3D myocardium strain on clinical cine MRI of two adult patients. Results showed that incompressibility constraint improves the cardiac motion recovery when compared to the ground truth provided by 3D tagged MRI.     

A Formally Verified Compiler Back-end

This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its soundness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.     

A subject-specific software solution for the modeling and the visualization of muscles deformations

Today, to create and to simulate a virtual anatomical version of a subject is useful in the decision process of surgical treatments. The muscular activity is one of the factors which can contribute to abnormal movements such as in spasticity or static contracture. In this paper, we propose a numerical solution, based on the Finite Element (FE) method, able to estimate muscles deformations during contraction. Organized around a finite element solver and a volumetric environment, this solution is made of all the modeling and simulation processes from the discretization of the studied domain to the visualization of the results. The choices of materials and properties of the FE model are also presented such as the hyperelasticity, the contention model based on inter-meshes neighboring nodes pairing, and the estimation of nodal forces based on the subject-specific muscular forces and action lines.

Conditional co-simulation of continuous and categorical variables for geostatistical applications

The modeling of uncertainty in continuous and categorical regionalized variables is a common issue in the geosciences. We present a hybrid continuous/categorical model, in which the continuous variable is represented by the transform of a Gaussian random field, while the categorical variable is obtained by truncating one or more Gaussian random fields. The dependencies between the continuous and categorical variables are reproduced by assuming that all the Gaussian random fields are spatially cross-correlated. Algorithms and computer programs are proposed to infer the model parameters and to co-simulate the variables, and illustrated through a case study on a mining data set.     

Coinductive big-step operational semantics

Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers. A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results.